package ch.epfl.lara.matcheck.verify.provers;

import ch.epfl.lara.matcheck.ast.Formula
import ch.epfl.lara.matcheck.verify.provers.formdecider.{FormDeciderWrapper,FormDeciderStringer}

object TheoremProvers  {   
  abstract class Prover {
    def apply(): Boolean
    def apply(f: Formula): ProverResults.ProverResult
    def asString(f: Formula): String 
  }
  final case object FormDecider extends Prover {
    override def apply(): Boolean = FormDeciderWrapper.init
    override def apply(f: Formula): ProverResults.ProverResult = FormDeciderWrapper.decide(asString(f))
    override def asString(f: Formula) = FormDeciderStringer(f)
    override def toString = "formDecider"
  }
  
  import scala.collection.mutable.HashMap;

  val provers = new HashMap[String, Prover]();
  
  provers += "formdecider" -> FormDecider
  
  
  def string2prover(name: String): Prover = 
    provers.getOrElse(name.toLowerCase,error("'" + name + "' is not supported"))
 
}
